|
In computer science, the Davis–Putnam–Logemann–Loveland (DPLL) algorithm is a complete, backtracking-based search algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e. for solving the CNF-SAT problem. It was introduced in 1962 by Martin Davis, Hilary Putnam, George Logemann and Donald W. Loveland and is a refinement of the earlier Davis–Putnam algorithm, which is a resolution-based procedure developed by Davis and Putnam in 1960. Especially in older publications, the Davis–Logemann–Loveland algorithm is often referred to as the “Davis–Putnam method” or the “DP algorithm”. Other common names that maintain the distinction are DLL and DPLL. After almost 50 years the DPLL procedure still forms the basis for most efficient complete SAT solvers. It has recently been extended for automated theorem proving for fragments of first-order logic.〔 〕 == Implementations and applications == The SAT problem is important both from theoretical and practical points of view. In complexity theory it was the first problem proved to be NP-complete, and can appear in a broad variety of applications such as ''model checking'', automated planning and scheduling, and diagnosis in artificial intelligence. As such, it was and still is a hot topic in research for many years, and competitions between SAT solvers regularly take place.〔 〕 DPLL's modern implementations like Chaff and zChaff,〔 〕〔 〕 GRASP or Minisat〔 〕 are in the first places of the competitions these last years. Another application which often involves DPLL is automated theorem proving or satisfiability modulo theories (SMT) which is a SAT problem in which propositional variables are replaced with formulas of another mathematical theory. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「DPLL algorithm」の詳細全文を読む スポンサード リンク
|